// #include "assert.h"
#include "list.h"
#include <math.h>
void ESBMC_assert(int condition);

int main()
{
    double v1 = 1;
    double v2 = 2;
    double x1 = 690, x2 = 0;
    list_t *mylist = list_new();
    list_node_t *node = list_node_new("my value");
    node->prev = NULL;
    list_rpush(mylist, node);
    list_node_t *node2 = list_node_new("my value2");
    list_rpush(mylist, node2);
    list_node_t *node3 = list_node_new("my value2");
    list_rpush(mylist, node3);

    int length = mylist->len;

    for (int i = 0; i < 10; i++)
    {
        // CBMC在使用定界循环时效率较高
        for (int j = 0; j < length; j++)
        {
            x1 = x1 + fabs(sin(x1)*5);
            x2 = x2;
        }

        assert(x1 > x2);
    }
}
